@SuperSandro2000 any chance I could trouble you to review this? I think it should be straightforward, I did it the same way as other Jupyter kernels I've packaged in the past.

@siraben don't you know coq?

I do, but I'm not very familiar with Jupyter. I'll review this when I have some time.

Any chance we can get this merged soon? Coq familiarity isn't really required, you just have to start up the Jupyter notebook and confirm that it successfully runs Coq code. It works for me when doing the following:

nix run nixpkgs#nixpkgs-review pr 171202
$(nix-build -E 'with import ./. {}; jupyter.override { definitions = { coq = coq-kernel.definition; }; }')/bin/jupyter-notebook

@SuperSandro2000 @siraben ping again on this.

I confirm that I can start the notebook and run Coq code. How would one go about adding coqPackages?

Currently a dependency is broken for which I opened a PR #205043.

I was actually looking at the metakernel breakage yesterday and realized coq_jupyter doesn't actually require it. Just removed it and rebased on master.

How would one go about adding coqPackages?

I'm not sure, the manual seems to only describe how to add new ones. If you figure it out please lmk!

Actually, it seems like coqPackages are meant to be installed alongside coq in the same environment. For example, if I build coqPackages.ceres, it produces a lib path result/lib/coq/8.16/user-contrib/Ceres. Presumably coq will search these kinds of paths when you do an Import.

However, it's not working too well for me. I tried installing coq alongside coqPackages.ceres, and the import still failed. I notice coq alone produces lib/coq/user-contrib so perhaps there's a slight mismatch here.

EDIT: it does work in coqide though. That must be setting up search paths differently.

Aha I figured it out, based on the bullet point about extraInstallFlags here: https://nixos.org/manual/nixpkgs/stable/#coq-packages-attribute-sets-coqpackages.

Just pushed a commit adding a definitionWithPackages function.

Just pushed a commit adding a definitionWithPackages function.

That should be pretty useful. Pinning versions is common in this space, so could you also make the coq version configurable? I would like to pass say coq_8_15 along with some coqPackages_8_15. I will test it again after that, and then it should be ready before more feature creep sets in ;)

I think it's already configurable via override, which AFAIK is the standard pattern.

What I'd really like to do is open a PR to either attach the coqPackages for a given version to the coq, or even better, add a coq.withPackages function.

I've tested it with adding some coqPackages and also overriding the coq version. Everything works so it LGTM.

Great! Let's see if we can get it merged now.

@SuperSandro2000 ? This is still ready to go

Hi @jonringer, I'm hoping to find a reviewer for this and a few other Jupyter-related PRs. I saw you committed the initial IRuby PR so I was wondering if you could take a look here?

I've just updated this to be consistent with the latest Jupyter stuff. I think it's ready to merge!

Could you rebase your changes with the latest nixpkgs?

Done @GTrunSec

Test: nix run --impure --expr 'with import ./. {}; jupyter-console.withSingleKernel (coq-kernel.definitionWithPackages [coqPackages.bignums])'

nix run --impure --expr 'with import ./. {}; jupyter-console.withSingleKernel (coq-kernel.definitionWithPackages [coqPackages.bignums])'
Jupyter console 6.6.3

The Coq Proof Assistant, version 8.18.0
compiled with OCaml 4.14.1

In [1]: Compute (1 + 1).
Out[2]:
     = 2
     : nat

Thanks, LGTM

Cool! I guess now we ping @teto that this kernel is ready to go?

we should ping @natsukium jupyter team.